structure Proof =
struct
  structure Asst = Assert
  structure Asm = Assem
  
  type lemma = string
  type lab = string

  datatype prf_blk
    = WF_addr of Asm.reg * Asm.reg *((Asm.instr list) * prf_blk) * (Asst.assert * Asst.assert * lemma)
    | WF_jmp of lab * (Asst.assert * Asst.assert * lemma)
    | WF_trivial

  datatype atype
    = Prop of Asst.prop
    | Stype of Asst.st

  datatype pterm
    = Func of (string * atype) * pterm  (* (arg_id, arg_type, function_body) *)
    | Apply of pterm * pterm  
    | ID of string  (* function name (vc_name) *)
    | Exp of Asst.exp (* exp *)
end 
